es:ES, v:, x:Id, e:{e:E| @loc(e)(x:)} , e':{e':E| e loc e'  & (x after e') = v} .
((x when e) = (v)  )
 let e1 = next event in [e,e'] after which x = v in
 let e1e loc e1 
 let & e''[e,e1).(x after e'') = (v)  
 let & e''[e,e1].(x when e'') = (v)  
 let & (x after e1) = v
 let & (x when e1) = (v)   

latex

Definitions

True, T, @i(x:T), P  Q, P  Q, A, e[e1,e2].P(e), e[e1,e2).P(e), P  Q, , t  T, A c B, next event in [e,bound] after which x = b, let x = a in b(x), P  Q, e loc e' , P & Q, x:A. B(x), {T}, SQType(T), SqStable(P), False

Lemmas

true wf, squash wf, sq stable subtype rel, Id sq, es-loc-pred, decidable assert, es-isconst wf, sq stable from decidable, es-after-pred2, es-pred-locl, es-le-pred, es-pred wf, bnot wf, assert wf, not wf, cand functionality wrt iff, es-locl-iff, es-first wf, assert of bnot, es-locl irreflexivity, es-le weakening eq, es-locl transitivity2, es-le wf, es-next-assign wf, equal-bnot, event system wf, Id wf, es-dtype wf, es-E wf, es-le-loc, es-after wf, es-locl wf, es-vartype wf, es-loc wf, es-when wf, bool-deq wf, bool wf, es-next-assign-property